#!/bin/bash

# Inputs
INPUT_FILE=$1
THREADS=$2

# Outputs
OUTPUTS_DIRECTORY=outputs
TIME_RESULTS_FILE=$OUTPUTS_DIRECTORY"/"$INPUT_FILE".results_manysat"

# Executables
MANYSAT="/home/jaime/Dropbox/Mestrado/Pesquisa/Ursa/sat_solvers/manysat2.0/core/manysat2.0"

HEADER=`cat $INPUT_FILE | grep "p cnf"`

VARIABLES=`echo $HEADER | cut -d " " -f 3`
CLAUSES=`echo $HEADER | cut -d " " -f 4`


if [[ "$#" != 2 ]]
then
	echo "Wrong number of parameters. Expected 2." >&2
	exit 1
fi

if ! [[ -e "$MANYSAT" ]]
then
	echo "Could not find the solver." >&2
	exit 1
fi

echo "File = $INPUT_FILE" >> $TIME_RESULTS_FILE
echo "Formula has $VARIABLES variables and $CLAUSES clauses" >> $TIME_RESULTS_FILE

/usr/bin/time -o $TIME_RESULTS_FILE -a $MANYSAT $INPUT_FILE -ncores=$THREADS >> $TIME_RESULTS_FILE
echo >> $TIME_RESULTS_FILE
